k:FinProbSpace, x:Outcome, n:, X, Y:RandomVariable(k;n), a, b:.
rv-shift(x;a*X + b*Y) = a*rv-shift(x;X) + b*rv-shift(x;Y)  RandomVariable(k;n - 1) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), l[i], x. t(x), a  j < b. E(j), s = t, type List, , Type, True, n - m, -n, n+m, , T, S  T, cons-seq(x;s), f(a), r * s, r + s, x.A(x), X + Y, q*X, rv-shift(x;X), RandomVariable(p;n), Outcome, FinProbSpace
Lemmas	qadd wf, qmul wf, cons-seq wf, squash wf, true wf, le wf, nat plus wf, qsum wf, select wf, int seg wf, int inc rationals, length wf1, rationals wf